MIME-Version: 1.0
Server: CERN/3.0
Date: Sunday, 01-Dec-96 20:31:26 GMT
Content-Type: text/html
Content-Length: 2728
Last-Modified: Thursday, 01-Aug-96 17:12:28 GMT

<html>
<head>
<title>PRL Seminar talks</title>
</head>
<!--comment-->
<body>
<h1>PRL Seminars</h1>
<p>
Here are some of the slides for the talks I have given in the Nuprl
seminar.  These slides can be pretty technical, and assume knowledge
of the Nuprl system and type theory.  In some cases I
present information at an intuitive level that is technically imprecise.
<p>
All slides are in Portable Document Format (PDF).  You can obtain a
PDF reader from <a
href="http://www.adobe.com/acrobat/readstep.html">Adobe</a> for just about any machine you
can imagine using.  I prepared these presentations using <a
href="http://www.adobe.com/prodindex/persuasion/main.html">Adobe
Persuasion</a> and <a
href="http://www.adobe.com/prodindex/illustrator/main.html">Adobe Illustrator</a>.

<ul>
<li>
<!WA0><!WA0><!WA0><!WA0><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/mod2_96.pdf">Modules</a> February, 1996.  This is
my most recent version of formal modules and objects.
<li>
<!WA1><!WA1><!WA1><!WA1><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/mod10_95.pdf">Modules</a> October, 1995.  This
is an earlier version of formal modules.
<li>
<!WA2><!WA2><!WA2><!WA2><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/hor11_95.pdf">Horus</a> November, 1995.  We
are performing a verification of the <a
href="http://simon.cs.cornell.edu/Info/Projects/HORUS/">Horus group
communication system</a>.  These slides give an outline of the
verification process.
<li>
<!WA3><!WA3><!WA3><!WA3><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/typ10_94.pdf">Types</a> October, 1994.  These
slides cover some new type additions I was proposing for Nuprl.  This
includes very-dependent function types.
<li>
<!WA4><!WA4><!WA4><!WA4><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/sqrt5_94.pdf">Square Root Verification</a>
May, 1994.  This talk is about the verification of a hardware square
root algorithm by program transformation.  The slides don't contain
much explanation.  The <!WA5><!WA5><!WA5><!WA5><a href="http://www.cs.cornell.edu/Info/People/jyh/papers/tpcd94.ps">paper</a> we wrote
for <!WA6><!WA6><!WA6><!WA6><a href="http://goethe.ira.uka.de/tpcd94/toc.html">TPCD 1994</a>
(Theorem Provers in Circuit Design) is a better resource.
<li>
<!WA7><!WA7><!WA7><!WA7><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/thy3_94.pdf">Theories</a> March, 1994.  This
is a very early version of formal theories (modules) in Nuprl.
<li>
<!WA8><!WA8><!WA8><!WA8><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/vote11_93.pdf">Majority Vote</a> November,
1993.  This is the first formalization I did in Nuprl.  I gives some
idea of the problems I first encountered using Nuprl, and it provides
motivation for my current work in Nuprl.
</ul>

<h2>Some other talks.</h2>

<h3>Horus talks</h3>
<p>
<ul>
<li>
<!WA9><!WA9><!WA9><!WA9><a href="http://www.cs.cornell.edu/Info/People/jyh/horus/pi96.pdf">Horus Verification</a> January, 1996.  This
is a very high-level overview of the Horus verification effort.
<li>
<!WA10><!WA10><!WA10><!WA10><a href="http://www.cs.cornell.edu/Info/People/jyh/horus/hor4_96.pdf">Horus Verification</a> April, 1996.  Here
is a slightly more detailed, but still high-level, version of the Horus verification.
</ul>

</body>
